Artifact for "Partial Order Reduction for Reachability Games"

An artifact for the paper "Partial Order Reduction for Reachability Games", accepted at CONCUR'19. The source-code for the engine is found in the "verifypn-games.zip" file while the experiments and scripts to execute those are found in "reproducability.zip". Code The implementation reuses the general framework of partial order reduction applied in https://doi.org/10.1016/j.jlamp.2018.09.002 The core reduction algorithm is implemented in a (semantically equivalent and) efficient manner in PetriEngine/ReducingSuccessorGenerator.cpp Here the "prepare"-method implements the equivalent of the "St"-function of the paper (Algorithm 2), the "closure"-method implements the "Saturate"-function (Algorithm 3) and computeFinite, computeSCC, computeStaticCycles being responsible for the cycle-detection (Algorithm 1). Repeatability The repeatability-package is only available on Linux. To run the experiments as per the paper, run: ./run_POR.sh games-243 ; ./run_NPOR.sh games-243 Outputs will be generated in the "outputs" folder, and a Tex-table can be outputted by ./extract.sh games-243 Notice that we have pre-populated the outputs-folder with the results reported in the paper. The execution-scripts will NOT overwrite existing output files, and thus the outputs folder should be purged prior to a re-run of the experiments. To use a different executor (for instance sbatch on a slurm-enabled cluster for concurrent execution of the experiments), the run-commands can be prefixed as such: EXECUTOR=sbatch ./run_POR.sh games-243 The included binary is revision 243 of https://code.launchpad.net/~verifypn-cpn/verifypn/verifypn-games To limit the memory-consumption of each experiment, modify "run.sh" and change the "ulimit" memory-bound to the desired value. A "timeout"-command can also be added here to introduce a time-limit of the execution (we utilize slurm for this purpose). Notice that we measure and report the computation time excluding parsing; i.e. we report the fix-point computation-time as computed by the engine directly